p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))). rv-iid(p;n.f(n);n.X(n))   

latex

Definitions

t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), (x  l), r  s, x. t(x), xL. P(x), l[i], a  j < b. E(j), s = t, x:A  B(x), type List, , FinProbSpace, f(a), x(s), RandomVariable(p;n), Type, rv-identically-distributed(p;n.f(n);i.X(i)), rv-disjoint(p;n;X;Y), Outcome, S  T, suptype(S; T), , left + right, P  Q, A c B, r * s, (x.F(x)) o X, E(n;F), rv-iid(p;n.f(n);i.X(i)), x:A.B(x), Top, , A  B, , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), x,y:A//B(x;y), <a, b>, True, T

Lemmas

finite-prob-space wf, subtype rel function, squash wf, true wf, int seg properties, subtype rel weakening, ext-eq weakening, length wf nat, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, top wf, expectation wf, rv-compose wf, qmul wf, le wf, not wf, p-outcome wf, rv-disjoint wf, random-variable wf, nat wf, qsum wf, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf, length wf1, rationals wf